T:Type. subtype_rel(T; )  (L:(T List). sorted(L)  prop{i:l}) 

latex

Definitions	t  T, x:A. B(x), ||as||, P  Q, lelt(i; j; k), P  Q, False, A, A  B, int_seg(i; j), subtype(S; T), l[i], prop{i:l}, sorted(L)
Lemmas	int seg wf, le wf, select wf, length wf1